COMMENT ⊗   VALID 00018 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	.require "memo.pub[let,jmc]" source
C00004 00003	Abstract: Elephant is another language (like Lucid, Prolog and
C00006 00004	#. Introduction
C00010 00005	.<<old introduction>>
C00012 00006	#. Translating a sequential program into Elephant
C00019 00007	#. Reversing a list
C00024 00008	#. Non Immediate Elephant Programs
C00026 00009	#. An airline reservation system
C00030 00010	.if false then begin
C00034 00011	#. %2samefringe%1
C00038 00012	#. Parallel processes for computing a sum of functions
C00043 00013	#. Equivalence of Elephant programs.
C00049 00014	#. Remarks
C00055 00015	#. References
C00057 00016	.if false then begin
C00060 00017	.if false then begin "defining functions"
C00063 00018	.end
C00064 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.every heading (,incomplete draft,{page});
.at "qg" ⊂"%3go_to%*"⊃
.at "qNIL" ⊂"%1NIL%*"⊃
.turn on "→"
.group skip 15
.cb THE PROGRAMMING LANGUAGE ELEPHANT
.skip 1
.once center
by John McCarthy


.item←0
Abstract: Elephant is another language (like Lucid, Prolog and
first order recursive programs) that
represents programs as collections of sentences of first order logic.
Elephant differs from previous such languages in representing variables
explicitly as functions of time and in considering the %2program counter%1
or %2statement number%1 as just another variable.  Besides representing
ordinary sequential and parallel programs, Elephant can represent programs
that refer to the past of variables and therefore avoid explicit mention
of many data structures.  We argue that this feature is a necessary part
of a very high level language.  We also discuss proving properties of
Elephant programs and notions of equivalence of programs.
.skip to column 1
#. Introduction

	The Elephant algorithmic language
represents program variables as functions of a time variable.
Thus a variable ⊗x of an Algol program is replaced by a function
⊗x(t), and an assignment statement %2x_:=_...%1 is replaced by an
equation %2x(t+1)_=_...%1 or sometimes %2x(t)_=_...%1.  The Elephant
formalism has two uses.

	First, Elephant provides a simple way of expressing sequential
programs as sentences in a first order theory which can then be used to
prove properties of the program.  Elephant differs from the first order
representation of recursive programs described in (Cartwright 1976) and
(Cartwright and McCarthy 1979) in that Elephant is bottom-up instead of
top-down.  Once a program has been expressed in Elephant, the %2inductive
assertion%1 and %2intermittent assertion%1 methods are automatically
available as particular techniques of making proofs within first order
logic.  They amount to using particular kinds of lemmas in proving
theorems.  Instances of the Hoare axioms are probably also just lemmas.

	The second aspect of Elephant is the ability to refer to the
whole past of the variables without specifying data structures for
remembering what has to be known in order to perform a current action.
Thus a reservation program written in Elephant can say that a passenger
has a reservation if he has made one and not cancelled it without
specifying any data structure for remembering who has reservations.
Thus an elephant never forgets.

	This ability to refer to the past is certainly used in informal
English descriptions of what we want a computer to do.  Therefore, a
sufficiently high level programming language must have it.  On the other
hand, the Elephant programs that I have been able to write that refer
to the past are often more difficult to write and read than programs
with explicit data structures.  Perhaps I am simply inexperienced in
writing Elephant program, perhaps extensions to the formalism are
needed, and perhaps an approach different from Elephant will work better
in referring to the past.

	The simplest way to begin is with examples.

.<<old introduction>>
.if false then begin
#. Introduction

	The Elephant (it never forgets) algorithmic language
does assignment by regarding variables as explicit functions
of time; e.g. where Algol expects %2x_:=%1, Elephant expects %2x(t)_=%1.
The program counter is also explicitly regarded as a function of time.
Overcoming the inhibition against explicit use of time as the
independent variable allows programs to be represented as collections
of sentences in a first order logical language that can be used to
prove properties of the program.  Moreover, allowing the right hand
sides of equations to refer to other than the immediate past allows
"high level" programs that don't require data structure definitions
required by ordinary programming languages.
The concepts are best understood by means of examples.
The notation is as in (Cartwright and McCarthy 1979).
.end

#. Translating a sequential program into Elephant
.a←item

	Consider the following Algol 60 program fragment (declarations
are omitted) for doing multiplication by addition:

.begin nofill
%2

	i := n;				∂(30)0
	p := 0;				∂(30)1
loop:	qif i = 0 qthen qg done;	∂(30)2
	i := i - 1;			∂(30)3
	p := p + m;			∂(30)4
	qg loop;			∂(30)5
done:					∂(30)6
.end

The corresponding Elephant program consists of the equations

.begin nofill
.zz←12
%2

pc(0) = 0,

∀t.[i(t+1) →=_∂(zz)IF pc(t) = 0 THEN n
∂(zz)ELSE IF pc(t) = 3 THEN i(t) - 1
∂(zz)ELSE i(t)],

∀t.[p(t+1) →=_∂(zz)IF pc(t) = 1 THEN 0
∂(zz) ELSE IF pc(t) = 4 THEN p(t) + m
∂(zz)ELSE p(t)],

%1and%2

∀t.[pc(t+1) →=_∂(zz)IF pc(t) = 2 ∧ i(t) = 0 THEN 6
∂(zz)ELSE IF pc(t) = 5 THEN 2
∂(zz)ELSE pc(t) + 1].
.end

	In these equations ⊗i(t) and ⊗p(t) replace the simple
variables of the Algol program.  The function ⊗pc(t) is the
program counter, and it takes values from 1 to 6, corresponding
to the numbers written on the right of the Algol program.  It should
be apparent from the example that any program made up of assignments
and qgs can be systematically translated to an Elephant program.
We have used the logical conditional expression %2IF_..._THEN_..._ELSE%1
rather than qif_..._qthen_..._qelse, because there is no reason to
provide for an undefined case.  (The distinction is discussed in
(Cartwright and McCarthy 1979)).
If the reader is a reactionary and
refuses to admit conditional expressions as terms in first order
logic, then they can be eliminated.  The equation for ⊗i(t+1) would
then split into the three cases

.begin nofill
%2

∀t.[pc(t) = 0 ⊃ i(t+1) = 0 ∧ pc(t) = 1 ⊃ i(t+1) = i(t) - 1
∂9∧ pc(t) ≠ 0 ∧ pc(t) ≠ 1 ⊃ i(t+1) = i(t)]
.end

	Notice also that the length of the Elephant program is linear in the
length of the Algol program.

	Having one value of ⊗pc(t) for
each statement in the Algol program is unnecessary, although it makes
the systematic character of the translation more apparent.  If we
let %2pc(t)_=_0%1 correspond to the initialization, ⊗pc(t)_=_1 correspond
to the loop, and ⊗pc(t)_=_2 correspond to the label ⊗done, then the
equations become

.begin nofill
.zz←12
%2

pc(0) = 0,

∀t.[i(t+1) →=_∂(zz)IF pc(t) = 0 THEN n
∂(zz)ELSE IF pc(t) = 1 ∧ i(t) ≠ 0 THEN i(t) - 1
∂(zz)ELSE i(t)],

∀t.[p(t+1) →=_∂(zz)IF pc(t) = 0 THEN 0
∂(zz) ELSE IF pc(t) = 1 ∧ i(t) ≠ 0 THEN p(t) + m
∂(zz)ELSE p(t)],

%1and%2

∀t.[pc(t+1) →=_∂(zz)IF pc(t) = 1 ∧ i(t) ≠ 0 THEN 1
∂(zz)ELSE pc(t) + 1].
.end

	The correctness of the first version of the Elephant program is
given by the sentence

	%2∀m n ∃t.[pc(t) = 6 ∧ p(t) = mn]%1,

while the modified program would have the same correctness condition
except for having ⊗pc(t)_=_2 instead of ⊗pc(t)_=_6.  Either statement
is provable from any first order axiomatization of arithmetic
together with the sentences constituting the program.  No special
axioms for programs or "logic of programs" is required.

	Thus an entirely conventional mathematical way of writing
recursion equations leads to a convenient programming language.  I
am tempted to call the language Algol 50, since it could easily have
been developed at that time.

	The proof of correctness for this
multiplication program is misleadingly simple, since
we can easily write explicit formulas for ⊗i(t), ⊗p(t), and
⊗pc(t) and prove them by mathematical induction.  More typical proofs
occur when it isn't convenient to give explicit formulas for the
variables as functions of time or for the value of ⊗t for which the
program terminates.  Then the computational content of the proof is
is often essentially the same as that of an %2inductive assertions%1 proof
combined with induction on a rank function of the variables taking
values in a suitable inductively ordered set.

#. Reversing a list

	Reversing a list provides another example of an Elephant program
that can be compared with a recursive conditional expression program
for the same function.  We start with a Lisp "program feature" program
written in the style of Algol 60.
.begin nofill
%2
.z←8

∂zu := w;
∂zv := qNIL;
∂1loop:	∂zqif null u qthen qg done;
∂zv := [qa u] . v;
∂zu := qd u;
∂zqg loop;
∂1done:

.end

	The corresponding Elephant program is

.begin nofill
%2
.zz←12

pc(0) = 0,

∀t.[u(t+1) →=_∂(zz)IF pc(t) = 0 THEN w
		∂(zz)ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN qd u(t)
		∂(zz)ELSE u(t)],

∀t.[v(t+1) →=_∂(zz)IF pc(t) = 0 THEN qNIL
		∂(zz) ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN qa u(t) . v(t)
		∂(zz) ELSE v(t)]

∀t.[pc(t+1) →=_∂(zz)IF pc(t) = 1 ∧ ¬null u(t) THEN 1
		∂(zz)ELSE pc(t) + 1].
.end

	This can be compared with the LISP program ⊗reverse defined by

	%2reverse u ← qif qn u qthen qNIL qelse reverse qd u * <qa u>%1.

With the latter, as shown in (Cartwright and McCarthy 1979), it is
convenient to prove such properties as %2reverse_reverse_u_=_u%1 and
%2reverse[u_*_v]_=_reverse_v_*_reverse_u%1.  The major fact about
the Elephant program is expressed by

	%2∃t.(pc(t) = 2 ∧ v(t) = reverse w)%1.

It can be proved by proving that %2length u(t)%1 is a decreasing function
of ⊗t, i.e. for any ⊗t such that ⊗pc(t)_<_2, there is %2t'_>_t%1 such
that %2length_u(t')_<_length_t%1, and also that

	%2∀t.[reverse_w = reverse u(t) * v(t)]%1.

This is just another %2inductive assertions%1 proof.  So far it seems that
the most convenient technique for proving facts about Elephant programs
is %2inductive assertions%1,
which is less flexible than the technique described in (Cartwright and
McCarthy 1979) that uses the %2functional equation%1 and the %2minimization
schema%1.  This is because %2inductive assertions%1 provides no way
of expressing algebraic relations among functions defined by programs.

	One mathematically straightforward way of defining functions by
programs is the following.  We rewrite the above equations to introduce
⊗w as an explicit argument of the functions so that they become ⊗u(t,w), 
⊗v(t,w), and pc(t,w).  We then define a relation ⊗reverses(v,w) by

	%2∀v w.(reverses(v,w) ≡ ∃t.(pc(t,w) = 2 ∧ v(t,w) = v))%1.

When we have proved %2∀w ∃!v.reverses(v,w)%1, first order logic
entitles us to replace the relation ⊗reverses by a function.  We can
then prove successively that this function satisfies the relations

	%2reverse qNIL = qNIL%1,

	%2reverse [x . u] = reverse u * <x>%1

	%2reverse reverse u = u%1,

and

	%2reverse[u * v] = reverse v * reverese u%1,

where the notation is as in (McCarthy and Talcott 1979).

#. Non Immediate Elephant Programs

	When we translate an Algol program into Elephant, we get
equations in which the %2x(t+1)%1s depend only on the %2x(t)%1s.
We will call such a program an %2immediate%1 Elephant program.
However, the recursion
equations will still have guaranteed solutions if the %2x(t)%1s depend on
arbitrary earlier values of ⊗t.  This leads to a "high level" programming
language with the following features:

	1. The program refers to the past through earlier values of
⊗t, just as though everything were remembered.  That's why we call
the language Elephant, since an Elephant never forgets.

	2. The compiler is smart and decides what data structures are
required in order to carry out the computations without remembering
everything.  To the extent that compilers can be written that do this
effectively, Elephant is a "higher level" language in which the
programer specifies less than in Algol, etc.

#. An airline reservation system

	Consider programming a trivial airline reservation system.
We want to say that %2a passenger has a reservation if he
has made one that has not been cancelled%1.  We do not want to prescribe
what data structures have to be kept in order to be able to answer the
question of whether someone has a reservation.

	This program replies properly to requests to make reservations,
cancel them, and to inquiries about whether a reservation exists.
The program refers to its input in
terms of an abstract analytic syntax the meaning of whose mnemonic
predicate and function names is hopefully obvious.  The only data
structure explicitly mentioned is the number of seats currently occupied,
and even that could be eliminated from the program.  The Elephant compiler,
therefore, gets the honor of determining what other data structures
are needed.  We use the convention of writing %2α{xα}f%1 instead of ⊗f(x) when
it is convenient to write the argument before the function name.
.begin nofill
.uu←35

%2
∀t.[output(t+1) = α{input(t)α}[λ in.
∂(10)IF ismake in THEN →[∂(uu)IF hasrev(maker in,t) THEN "You had it"
			∂(uu)ELSE IF number(t) = N THEN "No room"
			∂(uu)ELSE "You have it now"]
∂(10)ELSE IF iscancel in THEN →[∂(uu)IF hasrev(maker in,t) THEN "It's cancelled"
			∂(uu)ELSE "You don't have it to cancel"]
∂(10)ELSE IF isinquiry in THEN→[∂(uu)IF hasrev(maker in,t) THEN "You have one"
			∂(uu)ELSE "You don't have one"]
∂(10)ELSE qNIL]

∀t.[number(t+1) = α{input(t)α}[λ in.
∂(10)IF ismake in THEN →[∂(uu)IF hasrev(maker in,t) ∨ number(t) = N
∂(uu)THEN number(t)
∂(uu)ELSE number(t) + 1]
∂(10)ELSE IF iscancel in THEN →[∂(uu)IF hasrev(maker in,t) THEN number(t) - 1
			∂(uu)ELSE number(t)]
∂(10)ELSE number(t)]
.end

where

	%2∀t.[hasrev(passenger,t) ≡ ∃t1.(t1 < t ∧ ismake input t1 ∧
passenger = maker input t1 ∧ number(t1) < N) ∧ ¬∃t2.(t1 < t2 < t ∧
iscancel input t2 ∧ maker input t2 = passenger))]%1.

	The main difficulty in making a compiler for Elephant is illustrated
by the predicate ⊗hasrev.  The compiler has to understand that it
must remember successful reservations but can forget unsuccessful
attempts at making a reservation and that it can forget reservations
that have been cancelled.  Perhaps ⊗hasrev should be written using primitives
that refer explicitly to the most recent occurrence of an event,
which might permit a less intelligent compiler.

.if false then begin
#. Elephant program to count vertices in a list structure

.begin nofill
****
There seems to be a bug in this program and the %2samefringe%1 program
that we hope to fix in a subsequent draft.
****
.end

	Another context in which it is possible to avoid specifying a
data structure by referring to the past, occurs when a list structure
is to be scanned.  The simplest example is a program to count the
vertices in a list structure.

Here ⊗a is the list structure being scanned, ⊗x is a running variable for
the current structure, and ⊗n is the current count.

	Because of Elephant's ability to refer to the past, we can
write this program without specifying a stack.  It is up to the compiler
to decide that a stack is appropriate for implementing the algorithm.

.begin nofill
%2 

∀t.[x(t+1) →=_∂(16)IF pc(t) =_0 THEN a
∂(16)ELSE IF pc(t) =_1 THEN
→[∂(22)IF [∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
∂(30)THEN x(t)
∂(22)ELSE IF ¬atom x(t) ∧ ¬seen(car x(t),t) then car x(t)
∂(22)ELSE cdr x(mostrecent(t,λt1.¬seen(cdr(x(t1)),t)))]
∂(16)ELSE x(t)]

∀t.[n(t+1) →=_∂(16)IF pc(t) =_0 THEN 0
∂(16)ELSE IF ∂(25)pc(t) =_1 
→∧ ∂(25)¬[∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
∂(30)THEN n(t) + 1
∂(16)ELSE n(t)]

∀t.[pc(t+1) →=_∂(16)IF ∂(20)pc(t) =_1
→∧ ∂(20)¬[∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
∂(25)THEN 1
∂(16)ELSE pc(t) + 1
.end

where the predicate ⊗seen and the functional ⊗mostrecent are defined as
follows:
.begin nofill
%2 

∀y t.[seen(y,t) ≡ ∃t1.[t1 ≤ t ∧ y =_x(t1)]]

∀t.[mostrecent(t, pred) = qif pred t qthen t qelse mostrecent(t - 1, pred)].
.end

We would like to regard these as definitions not as programs.  Indeed the
compiled program shouldn't compile them directly, but should do the job
another way that uses time and space more efficiently.

Of course, this example is less perspicuous than the Lisp program

%2count x ← qif qat x qthen 1 qelse count qa x + count qd x%1

which scans the vertices in the same order.  But then this problem
is especially appropriate for recursion and Lisp's built-in stack
mechanism.

Most likely ⊗seen and ⊗mostrecent will occur in other algorithms
where one doesn't want to look at things that have been already tried.

#. %2samefringe%1

	The LISP predicate %2samefringe[x,y]%1 may be defined by

%2samefringe[x1,x2] ≡ fringe x1 = fringe x2%1,

where %2fringe_x%1 is a list of the atoms in ⊗x and is defined by

%2fringe x ← qif qat x qthen <x> qelse fringe qa x . fringe qd x%1.

	The above definition does not provide the most efficient
computation of ⊗samefringe, and a better LISP function is given
in (Cartwright and McCarthy 1979), and a proof of its correctness
is outlined.  A detailed computer-checked proof is given in
(Talcott 1979).

	The following is an Elephant program for %2samefringe%1.

.begin nofill
%2
.a←12;b←28;c←35;

pc(0) = 0

∀t.[x1(t+1) →=_∂aIF pc(t) = 0 THEN x1
∂aELSE IF pc(t) = 1 THEN
→[∂bIF [∃y.seen1(y,t) ∧ ¬atom y ∧ [¬seen1(car y,t) ∨ ¬seen1(cdr y,t)]
∂cTHEN cdr x1(mostrecent(t,λt1.¬seen1(cdr(x1(t1)),t)))
∂bELSE x1(t)]
∂aELSE IF pc(t) = 2 THEN
→[∂bIF [∃y.seen1(y,t) ∧ ¬atom y ∧ [¬seen1(car y,t) ∨ ¬seen1(cdr y,t)]
∂cTHEN cdr x1(mostrecent(t,λt1.¬seen1(cdr(x1(t1)),t)))
∂b ELSE IF ¬atom x1(t) THEN car x1(t)
∂b ELSE x1(t)]
∂a ELSE x1(t)]

∀t.[x2(t+1) →=_∂aIF pc(t) = 0 THEN x2
∂aELSE IF pc(t) = 1 THEN
→[∂bIF [∃y.seen2(y,t) ∧ ¬atom y ∧ [¬seen2(car y,t) ∨ ¬seen2(cdr y,t)]
∂cTHEN cdr x2(mostrecent(t,λt1.¬seen2(cdr(x2(t1)),t)))
∂bELSE x2(t)]
∂aELSE IF pc(t) = 2 THEN
→[∂bIF [∃y.seen2(y,t) ∧ ¬atom y ∧ [¬seen2(car y,t) ∨ ¬seen2(cdr y,t)]
∂cTHEN cdr x2(mostrecent(t,λt1.¬seen2(cdr(x2(t1)),t)))
∂b ELSE IF ¬atom x2(t) THEN car x2(t)
∂b ELSE x2(t)]
∂a ELSE x2(t)]

∀t.[pc(t+1) →=_∂aIF (pc(t) = 1 ∨ pc(t) = 2 ∧ atom x1(t) ∧ atom x2(t) ∧ x1(t) ≠ x2(t)
∂bTHEN 4
∂aELSE IF pc(t) = 2 ∧ atom x1(t) ∧ atom x2(t) THEN 1
∂aELSE IF ∂bpc(t) = 1
→∧_∂b∀y.[seen1(y,t) ⊃ atom y ∨ seen1(car y,t) ∧ seen1(cdr y,t)]
→∧_∂b∀y.[seen2(y,t) ⊃ atom y ∨ seen2(car y,t) ∧ seen2(cdr y,t)]
∂cTHEN 5
∂aELSE IF ∂bpc(t) = 1
→∧_[∂b∀y.[seen1(y,t) ⊃ atom y ∨ seen1(car y,t) ∧ seen1(cdr y,t)]
→∨_∂b∀y.[seen2(y,t) ⊃ atom y ∨ seen2(car y,t) ∧ seen2(cdr y,t)]]
∂cTHEN 4
∂a ELSE pc(t) + 1]

%1where%2

∀y t.[seen1(y,t) ≡ ∃t1.[t1 ≤ t ∧ y =_x1(t1)]]

%1and%2

∀y t.[seen2(y,t) ≡ ∃t1.[t1 ≤ t ∧ y =_x2(t1)]].

.end

	As Thurber might have put it, compared to the recursive definition,
this is a little big and pretty ugly.  However, it does have a certain
brute force straightforward character, and it certainly leaves to the
compiler the task of inventing suitable data structures.

	The theorem to be proved is

%2(samefringe(x1,x2) ≡ ∃t.(pc(t) = 5)) ∧ (¬samefringe(x1,x2) ≡ ∃t.(pc(t) = 4))%1.
.end

#. Parallel processes for computing a sum of functions

.begin
.turn on "[]↑↓&"
.font B "BDJ20"

	The following Elephant program computes %AS%B↑N&↓[n=1]%2f(n))%1
using ⊗k processors.  A master processor with program counter ⊗pc(t) 
initializes the variables ⊗n and ⊗s and starts the ⊗k slave
processes whose program counters are written ⊗pc(i,t) 
at step 1.  A process needs exclusive access to ⊗n when
it is reading it and incrementing it, and it needs exclusive access
to ⊗s when incrementing it, and we only provide for exclusive access
at these times.  We imagine that computing ⊗f(n) takes ⊗time(n) units
of time, and these operations are done in parallel.  ⊗pc(t) is the
program counter for the master process, and ⊗pc(i,t) is the program
counter of the %2i%1th slave process.  The updating of all variables
except the ⊗pc(i,t) works as in Algolic programs, but the latter
requires a more elaborate and somewhat implicit description that may
well challenge the designer of an Elephant compiler.
.end

.begin nofill
.ww←10
%2 

n(t+1)→=_∂(ww)IF pc(t) = 0 THEN 1
∂(ww)ELSE IF pc(i,t) = 1 ∧ n(t) ≤ N THEN n(t) + 1
∂(ww)ELSE n(t)

s(t+1)→=_∂(ww)IF pc(t) = 0 THEN 0
∂(ww)ELSE IF pc(i,t) = 5 THEN s(t) + m(i,t)
∂(ww)ELSE s(t)

m(i,t+1)→=_∂(ww)IF pc(i,t) = 3 ∧ n(t) ≤ N THEN n(t)
∂(ww)ELSE IF pc(i,t+1) = 4 THEN f(m(i,t))
∂(ww)ELSE m(i,t)

pc(t+1) →=_∂(ww)IF pc(t) = 1 ∧ ∃i.(pc(i,t) ≠ 0) THEN 1
∂(ww)ELSE pc(t) + 1


pc(i,0) = 0

pc(i,t) = 0 ⊃ pc(i,t+1) = IF pc(t) = 0 THEN 1 ELSE 0

pc(i,t) = 1 ⊃ ∃!j.(pc(j,t) = 1 ∧ pc(j,t+1) = 2) ∧ ∃t'.(t < t' ≤ t+k ∧ pc(i,t') = 2)

pc(i,t) = 1 ⊃ pc(i,t+1) = 1 ∨ pc(i,t+1) = 2

pc(i,t) = 2 ⊃ pc(i,t+1) = IF n(t) ≤ N THEN 3 ELSE 0

pc(i,t) = 3 ∧ pc(i,t-1) ≠ 3 
∂(ww)⊃ ∀t'.(t ≤ t' < t + time(m(i,t)) ⊃ pc(i,t') = 3) ∧ pc(t+time(m(i,t))) = 4

pc(i,t) = 4 ⊃ ∃!j.(pc(j,t) = 4 ∧ pc(j,t+1) = 5) ∧ ∃t'.(t < t' ≤ t + k ∧ pc(i,t') = 5)

pc(i,t) = 5 ⊃ pc(i,t+1) = 1
.end

	It may be questioned whether the above Elephant program should be
regarded as a "program" that can be compiled by a suitable compiler or as
something between a specification and a program.  Perhaps it is an example
of that elusive concept called an algorithm.  Notice that it assumes that
synchronization occurs without specifying any way of doing it.  Just the
thing to challenge a smart compiler or automatic programming system.  On
the other hand, the correctness of the Elephant program is given by the
statement,

.begin nofill
.turn on "[]↑↓&"
.font B "BDJ20"

%2∃t.(pc(t) = 2 ∧ ∀i(pc(i,t) = 0) ∧ s(t) = %AS%B↑N&↓[n=1]%2f(n))%1
.end

and this can presumably be proved from the program.  The correspondence
between this Elephant program and one that is more explicit about
synchronization might be proved separately.

	There may well be better ways of describing parallel processes
in Elephant.

#. Equivalence of Elephant programs.

.begin
.turn on "↓"
.at "uu" ⊂"%3u%*"⊃
.at "vv" ⊂"%3v%*"⊃
.at "xx" ⊂"%3x%*"⊃
.at "yy" ⊂"%3y%*"⊃

	Definitions of the equivalence of Elephant programs,
equivalence-preserving transformations of programs, and techniques for
proving equivalence can be expected to be important in applications of
Elephant.  For example, one approach to compiling Elephant is to transform
the program into an immediate program using equivalence-preserving
transformations.

	Equivalence relations should be defined that will facilitate
this process.  An obvious form of equivalence is to require that each
variable in the two programs be represented by the same function of
time for all values of the parameters.  This is too strict an equivalence
to be interesting on two grounds.  First, the two forms of the multiplication
by addition program in section 2 would not be equivalent, because
one of them goes around the loop in one time step while the other takes
four steps.  Second, transforming a program to an immediate program may
involve the introduction of new variables, arrays and other data structures
in order to eliminate the direct references to the past.

	We cannot %2a priori%1 exclude the possibility that several
concepts of equivalence will be useful.  However, our first attempt
is based on the idea that correspondence of times doesn't matter so
long as the correspondence is monotonic and that we are interested only
a certain correspondence between the states of the program.

	Let one Elephant program ⊗P have functions ⊗u↓1(t),_..._,u↓m(t) and
a second ⊗P' have functions ⊗u↓1'(t)_..._u↓n'(t).  In order to avoid prolixity,
we shall summarize these functions as vectors %2uu(t)%1 and %2uu'(t)%1.  Let
%2EP(uu,uu')%1 be a relation.  Let the first depend on
parameters %2x↓1,_..._x↓p%1 and the second have parameters %2x↓1'_..._x↓q'%1,
similarly summarized into vectors %2xx%1 and %2xx'%1.
(The parameters of the program for multiplication by addition were ⊗m and ⊗n). 
Let %2EP(xx,xx')%1 be a relation between the parameters.
Also let %2I(xx)%1 and %2I'(xx')%1 be predicates that say what states of the
two programs are to be compared.
Now suppose we can prove that

	%2P ∧ P' ∧ EP(xx,xx') ⊃ EV(uu(0),uu'(0)) ∧ I(uu(0)) ∧ I'(uu'(0))%1

and

	%2P ∧ P' ⊃ ∀t1 t2 t1'.[EV(uu(t1),uu'(t1')) ∧ t2 >t1 ∧ I(uu(t2))
 ⊃ ∃t2'.EV(uu(t2),uu'(t2'))]%1

and going the other way

	%2P ∧ P' ⊃ ∀t1 t1' t2'.[EV(uu(t1),uu'(t1')) ∧ t2' >t1' ∧ I'(uu'(t2'))
 ⊃ ∃t2.EV(uu(t2),uu'(t2'))]%1.

We should then call the programs ⊗P and ⊗P' equivalent with respect
to the the conditions ⊗I and ⊗I' and the relations ⊗EP and ⊗EV. 
Note that we have used the programs themselves as hypotheses since we can
regard a program as the conjunction of its constituent sentences.

	The two versions of multiplication by addition are equivalent
with respect to the predicates

	%2EP(m,n,m',n') ≡ m=m' ∧ n=n'%1

and

	%2EV(i,p,pc,i',p',pc') ≡ (pc=0 ∧ pc'=0) ∨
[i=i' ∧ p=p' ∧ (pc=2 ∧ pc'=1 ∨ pc=6 ∧ pc'=2)]%1

They should be sufficient to prove that one program is correct (according
to the definitlons of section 2) if and only if the other is.
We expect to give less trivial examples of equivalence and maybe a proof
of equivalence in the final version of this paper.
.end

	Input-output equivalence, i.e. that two programs give the same
output sequence for any sequence of inputs, seems to be a special case of the
above, and there
is reason to hope that it will
suffice for many applications.

#. Remarks

1. Programs in Lucid (Ashcroft and Wadge 1976) are also collections of sentences 
in a first order language.  A Lucid object is a vector of the values 
of a variable throughout time.  This permits some statements to be
made in a very neat way.  However, it seems to be less flexible than
the Elephant device of admitting the time as an explicit parameter.
Lucid programs do not admit qgs, and there are other unexpected
restrictions.  Perhaps some of Lucid's problems would be cured by
including the history of the program counter as a variable.

2. The properties of Elephant programs don't depend on time taking
integer values.  All we need require is that the set of times be ordered
and unbounded above.  Then the first sentence of the product program
would take the form
.begin nofill
.u←20

%2∀t ∃t'.[t' > t ∧ i(t') →=_∂uIF pc(t) = 0 THEN n
∂uELSE IF pc(t) = 3 THEN i(t) - 1
∂uELSE i(t)].
.end

3. It seems to me that any language that purports to allow the user to say
what he wants the computer to do in English, should allow the executive or
general or other big shot to say that %2a customer has a reservation if he
has made one and it hasn't been cancelled%1.  The big shot certainly
doesn't want to concern himself with what data structures are required in
order to fulfill his wishes, and Elephant shows that his wishes can be
stated without mentioning such a data structure.

4. In its present state, Elephant doesn't seem to be a very easy
language to use.  I say "seem", because the awkward programs may
be merely a consequence of inexperience.  Of course, Algolic programs
are easy enough to write in Elephant.

5. Regarded simply as a way of writing Algolic programs as logical
sentences, Elephant plays a role similar to that played by
the Cartwright way of writing Lisp style
recursive conditional expression programs as logical sentences.
In fact it may be
a kind of dual to the Cartwright method just as %2inductive
assertions%1 and %2subgoal induction%1 seem to be duals.  Namely, Elephant
programs and inductive assertions work from an initial state and
describe its changes, while Lisp style programs and subgoal induction
work backwards from desired final result.  Thus it may complete a
pattern of methods of program formalization.

6. Elephant may be expanded by relaxing the restriction that statements
refer only to the past.  Our big shot may wish to say, %2"When the
passengers arrive at the airport for the flight,
an airplane and a crew will have been summoned by
the scheduling program to fly them to their destination"%1.
Allowing the right hand sides of Elephant equations to refer
to the future puts a heavier burden on the compiler.  In fact,
a futuristic Elephant program may be contradictory and hence
uncompilable.  Thus a compiler for futuristic Elephant is really
a kind of problem solver.  Only the future can tell if this style
of programming will prove useful or even theoretically illuminating.

7. The two aspects of Elephant, explicit use of the time and program
counter and reference to the past, may be separated.  The first all
by itself provides the proper formalization of sequential programs,
and there are probably other ways of referring to the past than
by using an explicit time variable, e.g. modal tense operators might
be used.  One of these ways might be more convenient.

8. Church (1957) represents digital circuits as recursive systems of Boolean
equations determining the behavior of a collection of Boolean
variables as a function of time.  He discusses the synthesis of circuits
with given behavior.  Some of his results might lead to theorems
about classes of Elephant programs over finite domains in cases where
the finiteness of the domain is important.
#. References

%3Ashcroft, E. A. and W. W. Wadge (1976)%1: Lucid - A Formal System
for Writing and Proving Programs, %2Siam Journal of Computing%1,
Vol. 5, No. 3, September.

%3Cartwright, R.S. (1976)%1:
%2A Practical Formal Semantic Definition and Verification System
for Typed Lisp%1,
Ph.D. Thesis, Computer Science Department, Stanford University,
Stanford, California.

%3Cartwright, Robert and John McCarthy (1979)%1: "Recursive Programs
as Functions in a First Order Theory", in E. Blum and S. Takasu (eds.),
%2Proceedings of the International
Conference on Mathematical Studies of Information Processing%1, Springer
Publishers.

%3Church, Alonzo (1957)%1: "Application of Recursive Arithmetic to the
Problem of Circuit Synthesis", in %2Summaries of talks presented at the
Summer Institute for Symbolic Logic, Cornell University 1957%1.,
Institute for Defense Analyses.

%3Kroger, F. (1978)%1: "A Uniform Logical Basis for the Description,
Specification and Verification of Programs", in E.J. Neuhold (ed.),
%2Formal Descriptions of Programming Concepts%1, North-Holland.

%3McCarthy, John and Carolyn Talcott (1979)%1: 
%2LISP: Programming and Proving%1,
(in preparation)
.if false then begin
Notes

1979 March 30

What concept of equivalence of Elephant programs should be used?

What should be proved about airline program?

Another example where data structure is not specified?
Maybe topological sort?
(General example: do not treat an item that has been previously treated)

Can elephant idea be extended to interacting parallel programs?

1979 March 31

Suppose a function is computed by an elephant program.  How does one
define the function and prove its properties?  Example: append or reverse.

How is a program equivalent to one which is obtained from it by
introducing a new variable and computing it?  We need a concept of
equivalence of programs w/r set of variables.  

Parallel programs

	Consider the following Algolic program in which two processes
co-operate in finding the largest element of an array.

.begin nofill
%2 
∂9n := 1; b := 0;	∂(40)0
∂9qg l1,l2;∂(40)1
l1:∂9if n = N qthen qg done;∂(40)2
∂9b := max(b,a[n]);∂(40)3
∂9n := n + 1;∂(40)4
∂9qgl1;∂(40)5

l2:∂9if n = N qthen qg done;∂(40)2
∂9b := max(b,a[n]);∂(40)3
∂9n := n + 1;∂(40)4
∂9qgl2;∂(40)5

done:∂(40)6
.end

The intent is that the two programs share the variables ⊗b and ⊗n and
merge when they reach ⊗done.  It is also important that they not
interfere with each other.  We can describe this process using
the ideas of Elephant as follows:

It looks like the matching problem provides a conundrum for tense logic
and perhaps there should be a new tense giving the time that matches a
given time.
.if false then begin "defining functions"
	We can define functions with Elephant programs as follows:

∀x.(∃y.P(x,y) ⊃ P(x,f(x)))

can always be written provided f is a fresh function symbol.  If we
can prove ∃!y.P(x,y), then we will be able to prove things about
the value of f(x).  In the specific Elephan context, we can write

∀x t.(pc(t,x) = done ∧ ∀t'.(t' < t > pc(t') ≠ done) ⊃ f(x) = y(t,x)),

and this axiomatizes a function f, saying nothing about it if the
program fails to terminate and defining it for those values of x
for which the program terminates.

	Actually, it is cleaner to write something that corresponds
more closely to the first definition, namely

∀x.(∃t.(pc(t,x) = done ∧ ∀t'(t' < t ⊃ pc(t')≠done))
		⊃ pc(tau(x),x) = done ∧ ∀t'.(t' < tau(x) ⊃ pc(t') ≠ done))

defining a function tau and the writing

∀x.(f(x) = y(tau(x),x)).

In this way we appeal only to the above simple principle.
.end "defining functions"
.end
.SKIP 1
This partial draft of ELEPHA[S79,JMC] compiled at {time} on {date}.